i:Id, X, T:Type, x0:X, P:(XTProp).
Normal(T)  Normal(X)  (x:X. Dec(v:T. P(x,v)))  es.pre-init1-p(es;i;"x";X;x0;"a";T;P) 

latex

Definitions

t  T, x:A. B(x), Consistent(R;es), x:AB(x), pre-init1-p(es;i;x;X;x0;a;T;P), P  Q, ES, "$x", Id, Type, Prop, x.A(x), x. t(x), preinit1R{$x:ut2, $a:ut2}(i; X; T; x0; P), Normal(T), f(a), x:AB(x), x:A. B(x), Dec(P), es.P(es), s.x, x : v, @i Precondition for a(v)P State(ds) (v:T), Realizer, type List, nil, @loc x initially v:T, car.cdr, State(ds), IdDeq, Void, x:A. B(x), Top, f(x)?z, hd(l), i<j, ij, l[i], #$n, a<b, AB, P & Q, i  j < k, False, A, {x:A| B(x) }, {i..j}, , @loc precondition for a(v:T):P State(ds) v, Normal(ds), a:A fp B(a), pre-p-realizable, EqDecider(T), Unit, left+right, IdLnk, EOrderAxioms(E; pred?; info), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), AtomFree(T;x), S  T, es-realizer(p), A  B, <a,b>, @i x initially v:T, tl(l), init-p-realizable, A & B, E, s = t, vartype(i;x), valtype(e), e@i. P(e), P  Q, ee'.P(e'), x initially@i

Lemmas

es-initially wf, init-p-realizable, atom-free wf, init-p wf, es-real-implies, R-sub-implies, normal-ds-single, es-realizer wf, pre-p-realizable, fpf wf, normal-ds wf, es-real wf, pre-p wf, R-sub-Rlist, select member, Rpre wf, le wf, fpf-cap-single, eqof eq btrue, id-deq wf, subtype rel self, decl-state wf, fpf-single wf, Rinit wf, es realizer wf, decidable wf, normal-type wf, Id wf, preinit1R wf, preinit1R feasible, implies-es-real, pre-init1-p wf, event system wf, R-consistent wf